Despite the availability of safe, high level languages, many of the most critical software systems are still written in low level programming languages such as C and C++. Although these low level programming languages are very expressive and can be used to write high performance code, such low level programming languages typically do not enforce type and memory safety. This makes low level programming languages much less robust and much more difficult to analyze than higher level languages.
Existing approaches to analyzing low level programs have included type checking and property checking. These approaches have encountered a number of problems and challenges. Type checking for lower level code is difficult because type safety often depends on subtle, program specific invariants. Although previous low level type systems can be quite expressive, they are typically designed for a fixed set of programming idioms and are hard to adapt to the needs of a particular program. Typical low level programs allow for declaring types, but such an approach does not hold the program to those declared types. As such, the program can still be compiled even if the types do not match. Consequently, type checking in low level programs typically checks some types and not others, leaving the program susceptible to errors.
A property checker is a tool for checking assertions over the state of a program. The assertions can be provided by means of preconditions and postconditions on procedures, as well as assumptions and assertions inside the program text.
Property checking tools for low level code can be quite powerful and quite general, but these tools either ignore types for soundness or rely on unproven type safety assumptions in order to achieve the necessary level of precision. For instance, it is difficult to write concise specifications that distinguish between locations in an untyped program's heap.
Consequently, there is a need for a sound and reliable approach for checking low level code.